The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

S tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

K tuples:none
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

MEMBER, EQ, CHOICE, GUESS, VERIFY, SAT, SATCK

Compound Symbols:

c3, c5, c8, c12, c14, c16, c17, c18

(3) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

S tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))

K tuples:

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

MEMBER, EQ, CHOICE, GUESS, VERIFY, SAT, SATCK

Compound Symbols:

c3, c5, c8, c12, c14, c16, c17, c18

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))

We considered the (Usable) Rules:

verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(nil, nil) → true
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
eq(O(z0), 0(z1)) → eq(z0, z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)

And the Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [3]   
POL(1(x₁)) = [3]   
POL(CHOICE(x₁)) = x₁   
POL(EQ(x₁, x₂)) = 0   
POL(GUESS(x₁)) = [2]x₁   
POL(IF(x₁, x₂, x₃)) = 0   
POL(MEMBER(x₁, x₂)) = 0   
POL(NEGATE(x₁)) = 0   
POL(O(x₁)) = 0   
POL(SAT(x₁)) = [2] + [5]x₁   
POL(SATCK(x₁, x₂)) = [2] + x₁   
POL(VERIFY(x₁)) = [2]   
POL(c12(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c16(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c5(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(choice(x₁)) = [2]x₁   
POL(cons(x₁, x₂)) = [1] + x₁ + x₂   
POL(eq(x₁, x₂)) = [4] + [2]x₂   
POL(false) = [5]   
POL(guess(x₁)) = [4] + [4]x₁   
POL(if(x₁, x₂, x₃)) = [2] + [3]x₂ + [4]x₃   
POL(member(x₁, x₂)) = [5] + [3]x₁ + [4]x₂   
POL(negate(x₁)) = 0   
POL(nil) = 0   
POL(true) = [3]   
POL(unsat) = [2]   
POL(verify(x₁)) = [1] + [4]x₁   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

S tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))

K tuples:

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))

Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

MEMBER, EQ, CHOICE, GUESS, VERIFY, SAT, SATCK

Compound Symbols:

c3, c5, c8, c12, c14, c16, c17, c18

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))

We considered the (Usable) Rules:

verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(nil, nil) → true
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
eq(O(z0), 0(z1)) → eq(z0, z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)

And the Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [2]   
POL(1(x₁)) = [2]   
POL(CHOICE(x₁)) = 0   
POL(EQ(x₁, x₂)) = 0   
POL(GUESS(x₁)) = 0   
POL(IF(x₁, x₂, x₃)) = 0   
POL(MEMBER(x₁, x₂)) = 0   
POL(NEGATE(x₁)) = [3]   
POL(O(x₁)) = 0   
POL(SAT(x₁)) = [1] + [5]x₁   
POL(SATCK(x₁, x₂)) = [4]x₂   
POL(VERIFY(x₁)) = [2]x₁   
POL(c12(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c16(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c5(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(choice(x₁)) = [1] + [2]x₁   
POL(cons(x₁, x₂)) = [2] + x₂   
POL(eq(x₁, x₂)) = 0   
POL(false) = 0   
POL(guess(x₁)) = x₁   
POL(if(x₁, x₂, x₃)) = [2]   
POL(member(x₁, x₂)) = [2]   
POL(negate(x₁)) = [3] + [4]x₁   
POL(nil) = 0   
POL(true) = 0   
POL(unsat) = [5]   
POL(verify(x₁)) = [3] + [2]x₁   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

S tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))

K tuples:

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))

Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

MEMBER, EQ, CHOICE, GUESS, VERIFY, SAT, SATCK

Compound Symbols:

c3, c5, c8, c12, c14, c16, c17, c18

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))

We considered the (Usable) Rules:

verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(nil, nil) → true
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
eq(O(z0), 0(z1)) → eq(z0, z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)

And the Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = x₁   
POL(1(x₁)) = x₁   
POL(CHOICE(x₁)) = 0   
POL(EQ(x₁, x₂)) = x₁   
POL(GUESS(x₁)) = [3]   
POL(IF(x₁, x₂, x₃)) = x₁   
POL(MEMBER(x₁, x₂)) = x₁·x₂   
POL(NEGATE(x₁)) = 0   
POL(O(x₁)) = [1] + x₁   
POL(SAT(x₁)) = [3] + [3]x₁ + [3]x₁²   
POL(SATCK(x₁, x₂)) = [2]x₂ + [3]x₂²   
POL(VERIFY(x₁)) = [3]x₁²   
POL(c12(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c16(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c5(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(choice(x₁)) = x₁   
POL(cons(x₁, x₂)) = [1] + x₁ + x₂   
POL(eq(x₁, x₂)) = x₁·x₂   
POL(false) = 0   
POL(guess(x₁)) = x₁   
POL(if(x₁, x₂, x₃)) = [2]x₂ + x₃   
POL(member(x₁, x₂)) = x₁·x₂   
POL(negate(x₁)) = [2]x₁   
POL(nil) = [1]   
POL(true) = 0   
POL(unsat) = 0   
POL(verify(x₁)) = 0   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

S tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))

K tuples:

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))

Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

MEMBER, EQ, CHOICE, GUESS, VERIFY, SAT, SATCK

Compound Symbols:

c3, c5, c8, c12, c14, c16, c17, c18

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))

We considered the (Usable) Rules:

verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(nil, nil) → true
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
eq(O(z0), 0(z1)) → eq(z0, z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)

And the Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [2] + x₁   
POL(1(x₁)) = [2] + x₁   
POL(CHOICE(x₁)) = 0   
POL(EQ(x₁, x₂)) = x₁·x₂   
POL(GUESS(x₁)) = x₁   
POL(IF(x₁, x₂, x₃)) = 0   
POL(MEMBER(x₁, x₂)) = x₁·x₂   
POL(NEGATE(x₁)) = 0   
POL(O(x₁)) = x₁   
POL(SAT(x₁)) = [2] + x₁ + [3]x₁²   
POL(SATCK(x₁, x₂)) = [1] + [2]x₂²   
POL(VERIFY(x₁)) = [1] + x₁²   
POL(c12(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c16(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c5(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(choice(x₁)) = x₁   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(eq(x₁, x₂)) = 0   
POL(false) = 0   
POL(guess(x₁)) = x₁   
POL(if(x₁, x₂, x₃)) = 0   
POL(member(x₁, x₂)) = x₂ + x₂² + x₁²   
POL(negate(x₁)) = x₁   
POL(nil) = [1]   
POL(true) = 0   
POL(unsat) = 0   
POL(verify(x₁)) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

S tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))

K tuples:

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))

Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

MEMBER, EQ, CHOICE, GUESS, VERIFY, SAT, SATCK

Compound Symbols:

c3, c5, c8, c12, c14, c16, c17, c18

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))

We considered the (Usable) Rules:

verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
eq(nil, nil) → true
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
eq(O(z0), 0(z1)) → eq(z0, z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)

And the Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = 0   
POL(1(x₁)) = 0   
POL(CHOICE(x₁)) = 0   
POL(EQ(x₁, x₂)) = 0   
POL(GUESS(x₁)) = [1]   
POL(IF(x₁, x₂, x₃)) = 0   
POL(MEMBER(x₁, x₂)) = [1] + x₂   
POL(NEGATE(x₁)) = 0   
POL(O(x₁)) = 0   
POL(SAT(x₁)) = [3] + [3]x₁²   
POL(SATCK(x₁, x₂)) = [1] + [2]x₂²   
POL(VERIFY(x₁)) = x₁²   
POL(c12(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c16(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄   
POL(c17(x₁, x₂)) = x₁ + x₂   
POL(c18(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c5(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(choice(x₁)) = 0   
POL(cons(x₁, x₂)) = [1] + x₂   
POL(eq(x₁, x₂)) = [2]   
POL(false) = 0   
POL(guess(x₁)) = x₁   
POL(if(x₁, x₂, x₃)) = 0   
POL(member(x₁, x₂)) = [2]x₁²   
POL(negate(x₁)) = 0   
POL(nil) = 0   
POL(true) = 0   
POL(unsat) = 0   
POL(verify(x₁)) = 0   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

S tuples:none
K tuples:

SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))

Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

MEMBER, EQ, CHOICE, GUESS, VERIFY, SAT, SATCK

Compound Symbols:

c3, c5, c8, c12, c14, c16, c17, c18

(15) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(16) BOUNDS(O(1), O(1))